The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
Term_sub, Sum_sub, Concat

They will be analysed ascendingly in the following order:
Sum_sub < Term_sub
Term_sub = Concat

(6) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

The following defined symbols remain to be analysed:
Sum_sub, Term_sub, Concat

They will be analysed ascendingly in the following order:
Sum_sub < Term_sub
Term_sub = Concat

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

Induction Base:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(0)) →_R^Ω(1)
Sum_term_var(hole_a3_0)

Induction Step:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(+(n12_0, 1))) →_R^Ω(1)
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) →_IH
Sum_term_var(hole_a3_0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

The following defined symbols remain to be analysed:
Concat, Term_sub

They will be analysed ascendingly in the following order:
Term_sub = Concat

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Concat(gen_Id:Cons_usual:Cons_sum10_0(n647_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n647_0), rt ∈ Ω(1 + n647₀)

Induction Base:
Concat(gen_Id:Cons_usual:Cons_sum10_0(0), gen_Id:Cons_usual:Cons_sum10_0(0)) →_R^Ω(1)
gen_Id:Cons_usual:Cons_sum10_0(0)

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum10_0(+(n647_0, 1)), gen_Id:Cons_usual:Cons_sum10_0(0)) →_R^Ω(1)
Cons_usual(hole_c7_0, Term_sub(Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(0)), Concat(gen_Id:Cons_usual:Cons_sum10_0(n647_0), gen_Id:Cons_usual:Cons_sum10_0(0))) →_R^Ω(1)
Cons_usual(hole_c7_0, Term_var(hole_b6_0), Concat(gen_Id:Cons_usual:Cons_sum10_0(n647_0), gen_Id:Cons_usual:Cons_sum10_0(0))) →_IH
Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(c648_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n647_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n647_0), rt ∈ Ω(1 + n647₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

The following defined symbols remain to be analysed:
Term_sub

They will be analysed ascendingly in the following order:
Term_sub = Concat

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250928_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250928₀)

Induction Base:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(0)) →_R^Ω(1)
Term_var(hole_b6_0)

Induction Step:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(+(n250928_0, 1))) →_R^Ω(1)
Term_sub(Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(n250928_0)) →_IH
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n647_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n647_0), rt ∈ Ω(1 + n647₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250928_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250928₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

The following defined symbols remain to be analysed:
Concat

They will be analysed ascendingly in the following order:
Term_sub = Concat

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Concat(gen_Id:Cons_usual:Cons_sum10_0(n532036_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n532036_0, b)), rt ∈ Ω(1 + b·n532036₀ + n532036₀)

Induction Base:
Concat(gen_Id:Cons_usual:Cons_sum10_0(0), gen_Id:Cons_usual:Cons_sum10_0(b)) →_R^Ω(1)
gen_Id:Cons_usual:Cons_sum10_0(b)

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum10_0(+(n532036_0, 1)), gen_Id:Cons_usual:Cons_sum10_0(b)) →_R^Ω(1)
Cons_usual(hole_c7_0, Term_sub(Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(b)), Concat(gen_Id:Cons_usual:Cons_sum10_0(n532036_0), gen_Id:Cons_usual:Cons_sum10_0(b))) →_L^{Ω(1 + b)}
Cons_usual(hole_c7_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), Concat(gen_Id:Cons_usual:Cons_sum10_0(n532036_0), gen_Id:Cons_usual:Cons_sum10_0(b))) →_IH
Cons_usual(hole_c7_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(+(b, c532037_0)))

We have rt ∈ Ω(n²) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n²).

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n532036_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n532036_0, b)), rt ∈ Ω(1 + b·n532036₀ + n532036₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250928_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250928₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(19) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
Concat(gen_Id:Cons_usual:Cons_sum10_0(n532036_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n532036_0, b)), rt ∈ Ω(1 + b·n532036₀ + n532036₀)

(20) BOUNDS(n^2, INF)

(21) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n532036_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n532036_0, b)), rt ∈ Ω(1 + b·n532036₀ + n532036₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250928_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250928₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(22) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
Concat(gen_Id:Cons_usual:Cons_sum10_0(n532036_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n532036_0, b)), rt ∈ Ω(1 + b·n532036₀ + n532036₀)

(23) BOUNDS(n^2, INF)

(24) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n647_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n647_0), rt ∈ Ω(1 + n647₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250928_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250928₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(25) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

(26) BOUNDS(n^1, INF)

(27) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n647_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n647_0), rt ∈ Ω(1 + n647₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(28) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

(29) BOUNDS(n^1, INF)

(30) Obligation:

Innermost TRS:
Rules:
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → a → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: a → Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: a → Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

(32) BOUNDS(n^1, INF)